/-
Copyright (c) 2025 Thomas R. Murrills. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Thomas R. Murrills
-/
module

public meta import Lean.Elab.Command
public import Lean.Linter.Basic
public import Lean.Environment
-- Import this linter explicitly to ensure that
-- this file has a valid copyright header and module docstring.
import Mathlib.Tactic.Linter.Header

/-!
# Private module linter

This linter lints against nonempty modules that have only private declarations, and suggests adding
`@[expose] public section` to the top or selectively marking declarations as `public`.

## Implementation notes

`env.constants.map₂` contains all locally-defined constants, and accessing this waits until all
declarations are added. By linting (only) the `eoi` token, we can capture all constants defined in
the file.

Note that private declarations from the current module are exactly those which satisfy
`isPrivateName`, whether private due to an explicit `private` or due to not being made `public`.

We also do not count declarations which satisfy `isReservedName` as public declarations *from the
current module*. While they might indeed be public, the declarations associated with reserved names
are generated automatically and lazily, sometimes in downstream modules from the one in which the
name was reserved.

For example, Lean might reserve the name `foo.eq_1` in one module, but only add a declaration with
the name `foo.eq_1` to the environment in some downstream module, when Lean attempts to
realize the name. If the original module is a `public import` of the downstream module, then this
new declaration `foo.eq_1` will be added to the public scope, as it would be if it had been
declared in the original module.

As such, if e.g. `simp` realized the public declaration `foo.eq_1` in some module `M.Bar`
downstream of the module in which `foo` was declared, but `M.Bar` did not add any other public
declarations, the linter should still fire on `M.Bar`. Ignoring reserved names ensures this.

See also the type `Lean.ReservedNameAction`, invocations of `registerReservedNameAction` and
`registerReservedNamePredicate` for examples, and the module `Lean.ResolveName` for further insight.

Note that metaprograms should not add public declarations when run in private scopes. Doing so would
likely be a bug in the metaprogram. As such, we do not perform further checks for automatically
generated declarations such as those in `isAutoDecl`.
-/

meta section

open Lean Elab Command Linter

namespace Mathlib.Linter

/-- The `privateModule` linter lints against nonempty modules that have only private declarations,
and suggests adding `@[expose] public section` or selectively marking declarations as `public`. -/
public register_option linter.privateModule : Bool := {
  defValue := false
  descr := "Enable the `privateModule` linter, which lints against nonempty modules that have only \
    private declarations."
}

/--
The `privateModule` linter lints against nonempty modules that have only private declarations,
and suggests adding `@[expose] public section` to the top.

This linter only acts on the end-of-input `Parser.Command.eoi` token, and ignores all other syntax.
It logs its message at the top of the file.
-/
def privateModule : Linter where run stx := do
  if stx.isOfKind ``Parser.Command.eoi then
    unless getLinterValue linter.privateModule (← getLinterOptions) do
      return
    if (← getEnv).header.isModule then
      -- Don't lint an imports-only module:
      if !(← getEnv).constants.map₂.isEmpty then
        -- Exit if any declaration from the current module is public:
        for (decl, _) in (← getEnv).constants.map₂ do
          -- Ignore both private and reserved names; see implementation notes
          if !isPrivateName decl && !isReservedName (← getEnv) decl then return
        -- Lint if all names are private:
        let topOfFileRef := Syntax.atom (.synthetic ⟨0⟩ ⟨0⟩) ""
        logLint linter.privateModule topOfFileRef
          "The current module only contains private declarations.\n\n\
          Consider adding `@[expose] public section` at the beginning of the module, \
          or selectively marking declarations as `public`."

initialize addLinter privateModule

end Mathlib.Linter
